We 


JavaYacas:

1. Eclipse-based worksheet for JavaYacas/macas
2. Gendut: Library for datastructures, syntax, algebra, and arithmetic
3. Macas: develop language (in Java) and engine
4. Integrate HOL-like prover
5. extend worksheet
6. Java-script-port of Macas


Ideas for language/worksheet:

* The basic language should be purely functional
* mathematical expressions should look "nice"
* scoping should not be too far from mathematical practice
* Reflection: syntactic objects (terms, expressions) should be accessible
* formal proof systems and should be independent from the core language
* at least one default formal system should be implemented: type theory or ZFC
* built-in structures (for instance matrices) should be formalizable
* it should be natural to mix formal proofs and natural language in the worksheet
* multithreading




For instance, a library may provide axioms and proofs in type theory, ZFC or natural language. In a worksheet, it should be possible to switch between those.

The main work is to develop a programming language (in particular scoping rules and syntax) where the mismatch between it and the formal proof system is not too big.

The language should be able to parse the following expressions and to give full reflexive access to them:


for all x in R: ... => ....

x^2+4

...


f(x) := ...

f(x) = g(x)


In most languages, function applications are different from variables in the sense that they are transient. The idea is to give functions
a special treatment: A function definition can always be deconstructed within the language itself, in the same way that composite
variables can be deconstructed. For instance, we can define:

f(x) = x^2

and than, because f always carries its definition, integrate symbolically:

g = integrate(f)

where the function integrate has access to f's definition.

Binding:

f(x) = 2 * g(x)

Maybe g schould'n be bound to f when it is not in the scope of f's definition?
Is the following idea feasible:

module fun {
  f(x) = ...  //functions from same module are always bounded
  g(x) = ...
} where +,*,0,1 from Nat ,//binds all occurences from Nat
  square, blub are free //optional: compiler error if other unbound variable occur

???


So in f(x) = x + 1, the symbols + and 1 are free variables!


(The interpreter console might have a standard environment, with bounded +,-,0,1, ....)

We can (recursively) bind free variables:

fNat = f where +,1 from Nat, none are free

For terms, the same rules apply (note that f(x) = is only another way of writing lambdas):

In 

cond = forall x. x > 0

the variables >, 0 are free.




At any rate, every function should have, as part of its definition, its bining context!


Every program text becomes a completely accessible syntactic structure. This is
one part of the language definition. But only a small part of those structures are executable. This part and its interpretation has to be defined.
The executable part of the language should be expressible enough to define all pre-defined structures (numbers, arrays etc.) but for efficiency
reasons we will implement many of those structures in a more efficient language. We will give full definitions in the core language for numbers and
arrays but those won't be used for the "real" code.

Assignment: (interprets square(y)):

x <- square(y)

Assignment of an expression:
x <- 'square(y)

in the following case, we assign a method to f:

f(x) = square(x)

same s

f <- lambda x.square(x)

lambda terms are never executed, they are always stored an accessible syntactic structure

what about

y <- 2
f <- lambda x.x+y

?

idea: y is replaced by its value from the local scope ('partially executed')

so 
f <- lambda x.x+y // effectively lambda x.x+2
and 
f <- 'lambda x.x+y  //no partial execution

are different.


While in interactive mode x might have (depending on y) 




